/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package core;

import core.Node.RESULT;
import domain.Domain;
import expression.Alias;
import expression.And;
import expression.Eq;
import expression.IntExpr;
import expression.Leq;
import expression.Lt;
import expression.Max;
import expression.Min;
import expression.Neq;
import expression.Not;
import expression.Or;
import expression.Sum;
import expression.Value;
import expression.VarInDomain;
import expression.Variable;
import heuristic.DomainHeuristic;
import heuristic.Heuristic;
import java.util.ArrayList;
import java.util.List;

/**
 *
 * @author usdtim
 */
public class Problem {

    private Heuristic heuristic;
    private List<Node> nodes;

    public Problem() {
        nodes = new ArrayList<Node>();
        nodes.add(new Node(this, null));
        heuristic = new DomainHeuristic();
    }
    
    public Problem(Heuristic h) {
        nodes = new ArrayList<Node>();
        nodes.add(new Node(this, null));
        heuristic = h;
    }

    /*
     *   ----------------------------------------
     *                  ACCESSEURS
     *   ----------------------------------------
     */
    public Heuristic getHeuristic() {
        return heuristic;
    }
    
    /*
     *   ----------------------------------------
     *                  SOLVE
     *   ----------------------------------------
     */
    private RESULT compute() {
        Node node = nodes.get(nodes.size()-1);
        
//        System.out.println("==================================================");
//        System.out.println("SOLVE: " + nodes.size());
//        System.out.println("==================================================");
//        System.out.println(node);
//        System.out.println("--------------------------------------------------");

        switch (node.solve()) {
            case UNSAT: {
//                System.out.println("===> UNSAT <===");
                return RESULT.UNSAT;
            }
            case SAT: {
//                System.out.println("===> SAT <===");
                return RESULT.SAT;
            }
            case UNKNOWN: {
//                System.out.println("===> UNKNOWN <===");
//                System.out.println(this);

                if (heuristic.select(node)) {
//                    System.out.println("===> HEURISTIC: " + heuristic);

                    // NEXT
                    Node nextNode = node.nextNode();
                    heuristic.nextConstraint(nextNode);
                    nodes.add(nextNode);
                    
                    // BACKTRACK
                    heuristic.backtrackConstraint(node);
                    
                    return RESULT.UNKNOWN;
                } else {
//                    System.out.println("Problem UNSAT");
                    return RESULT.UNSAT;
                }
            }
        }
        throw new UnsupportedOperationException("compute");
    }
    
    public boolean solve() {
        
        while (nodes.size() > 0) {
            switch (compute()) {
                case SAT: return true;
                case UNSAT: nodes.remove(nodes.size()-1);
            }
        }
        return false;
    }

    /*
     *   ----------------------------------------
     *                  INTERFACE
     *   ----------------------------------------
     */
    public void setConstraint(IntExpr i) {
        nodes.get(0).setConstraint(i);
    }
    
    public Variable createVariable(String v) {
        return nodes.get(0).createVariable(v);
    }
    
    public Alias createAlias(String n, IntExpr i) {
        return nodes.get(0).createAlias(n, i);
    }
    
    public Value createValue(int v) {
        return nodes.get(0).createValue(v);
    }

    public Leq createLeq(IntExpr a, IntExpr b) {
        return nodes.get(0).createLeq(a, b);
    }

    public Lt createLt(IntExpr a, IntExpr b) {
        return nodes.get(0).createLt(a, b);
    }

    public Eq createEq(IntExpr a, IntExpr b) {
        return nodes.get(0).createEq(a, b);
    }

    public Neq createNeq(IntExpr a, IntExpr b) {
        return nodes.get(0).createNeq(a, b);
    }

    public Sum createSum(IntExpr[] p) {
        return nodes.get(0).createSum(p);
    }

    public Sum createSum(IntExpr[] p, int v) {
        return nodes.get(0).createSum(p, v);
    }

    public Sum createSum(IntExpr p, int v) {
        IntExpr[] temp = { p };
        return nodes.get(0).createSum(temp, v);
    }

    public And createAnd(IntExpr[] p) {
        return nodes.get(0).createAnd(p);
    }
    
    public And createAnd(IntExpr a, IntExpr b) {
        IntExpr[] temp = {a, b};
        return nodes.get(0).createAnd(temp);
    }
    
    public Or createOr(IntExpr[] p) {
        return nodes.get(0).createOr(p);
    }
    
    public Or createOr(IntExpr a, IntExpr b) {
        IntExpr[] temp = {a, b};
        return nodes.get(0).createOr(temp);
    }
    
    public Not createNot(IntExpr p) {
        return nodes.get(0).createNot(p);
    }
    
    public VarInDomain createVarInDomain(Variable v, Domain d) {
        return nodes.get(0).createVarInDomain(v, d);
    }
    
    public Max createMax(IntExpr[] p) {
        return nodes.get(0).createMax(p);
    }
    
    public Max createMax(IntExpr a, IntExpr b) {
        IntExpr[] temp = {a, b};
        return nodes.get(0).createMax(temp);
    }
    
    public Min createMin(IntExpr[] p) {
        return nodes.get(0).createMin(p);
    }
    
    public Min createMin(IntExpr a, IntExpr b) {
        IntExpr[] temp = {a, b};
        return nodes.get(0).createMin(temp);
    }
    
    /*
     *   ----------------------------------------
     *                  PRETTY
     *   ----------------------------------------
     */
    public String toString() {
        return nodes.get(nodes.size()-1).toString();
    }
    
    public String getSolution() {
        if (nodes.size() > 0) {
            String s = "SOLUTION;\n";
            Node node = nodes.get(nodes.size()-1);
            
            for (Variable v: node.getVariables()) {
                s += v.pretty() + "\n";
            }

            for (Alias a: node.getAlias()) {
                s += a.pretty() + "\n";
            }
            
            return s;
        }
        else {
            return "NO SOLUTION";
        }
    }

}
